Interconnect optimization is a critical component of circuit design, and in particular, of Very Large Scale Integration (VLSI) circuit design. As part of interconnect optimization of a VLSI circuit design, repeaters (e.g., buffers and inverters) are used to reduce interconnect delay and to meet transition time/noise constraints. However, merely using repeaters does not solve all timing requirements; for example, when wire delay is greater than a clock cycle, the mere addition of repeaters may not solve the timing constraints and the insertion of flip-flops/latches is essential.
As a VLSI circuit is usually deeply pipelined and so the number of flip-flops in the circuit is significant, a design automation software tool is used to insert flip-flops in the circuit design to reduce the Register-Transfer-Level (RTL)-to-layout convergence time. Typically, the RTL specification determines the number of clock cycles required for each sender-receiver path in the design. When data from the sender logic requires more than one clock cycle to reach the receiver logic, a flip-flop is typically added to the RTL specification of the circuit design. Accordingly, an estimated flip-flop insertion count can be derived from the RTL design.
An automatic flip-flop insertion method can be used to implement the physical placement of the flip-flops based on the RTL specifications. The RTL design usually provides estimated quantity and locations of flip-flop insertions in the circuit merely to meet the latency constraints, e.g., based on distance and clocking cycles. Unfortunately, the RTL estimations usually do not match the physical implementations of flip-flop insertions in the subsequent physical design. The disagreement may force the designers to modify the physical design (such as placement or routing) or even logic design, which undesirably prolongs the RTL-to-layout convergence time.
After a flip-flop insertion process, RTL-to-gate logic equivalence checking is used to make sure the gate-level circuit does not alter functional behavior of the RTL. Particularly, if a path includes an odd number of inverters following a flip-flop insertion process, a logic error will occur. A conventional combinational equivalence check tool is typically used to verify equivalence between RTL and gate-level designs due to their high efficiency and good scalability. Unfortunately, most logic equivalence check (LEC) tools are only effective in verifying equivalences for combinational circuits within boundaries formed by sequential circuits on a path. Due to the lack of capability of comprehending logic across flip-flop boundaries, it is common that a LEC tool produces false non-equivalence results, such as false inversion errors.